
package agent.ccs
import scala.util.parsing.combinator._
import scala.util.matching.Regex
import scala.util.parsing.combinator.syntactical._
import scala.collection.immutable.HashMap
import com.sun.org.apache.xalan.internal.xsltc.compiler.ForEach
import scala.collection.mutable.LinkedList
import org.scalatest._
import org.scalatest.matchers.ShouldMatchers
import scala.util.parsing.input.CharSequenceReader
import cwb.Value
import cwb.CWBParseException
import com.sun.org.apache.xerces.internal.impl.xpath.regex.ParseException
import agent.AgentParser


// Agent builder
sealed trait agentBuilder {
  def completeAgent = false // false per default
}

case class prefixB(prefixList: List[Prefix]) extends agentBuilder

case class agentB(agent: PrivateAgent) extends agentBuilder {  
  override
  def completeAgent = true // TODO(gustafa): Check last element for whether it is an agent
}

// Expects ; to be cut off and \n stripped before taking the input.
class CCSParser extends AgentParser with RegexParsers {
  //var temp_agent = new AgentBuilder()
  protected def accepted: Parser[String] = """[a-zA-Z0-9]*""".r
  protected def upper: Parser[String] = """[A-Z]""".r
  protected def lower: Parser[String] = """[a-z]""".r
  protected val nullAgent: Parser[String] = "0"
    
    
  def agAccepted = """[a-zA-Z0-9']*""".r
  def actAccepted = accepted
  
  val restrictMax = 10
  var restrictCnt = 0
  def agentString: Parser[String] = upper ~ agAccepted ^^ {
    case x ~ y => x ++ y
  }
  
  def act: Parser[String] = lower ~ actAccepted ^^ {
    case x ~ y => x ++ y
  }
  def unbarredAct: Parser[prefixB] = act ^^ {
     x => new prefixB(List(new Prefix(Act(Symbol(x.toString()), true, None), Option(Symbol(x.toString)))))
  }
  
  def barredAct: Parser[prefixB] = "'" ~ act ^^ {
    case _ ~ x => new prefixB(List(new Prefix(Act(Symbol(x), false, None), Option(Symbol(x)))))
  }
  
  def tau: Parser[prefixB] = "tau" ^^ {
    case _ => new prefixB(List(new Prefix(new Tau(None), None)))
  }
  
  def an_act: Parser[prefixB] = tau | unbarredAct | barredAct
  
  
  def re_unbarred = act ^^ {
    case x => new Act(Symbol(x), true, None)
  }
  
  def re_barred = "'" ~ act ^^ {
    case _ ~ x => new Act(Symbol(x), false, None)
  }
  
  def re_tau: Parser[CCSAction] = "tau" ^^ {
    case _ => new Tau(None)
  }
  
  def relabelAct: Parser[CCSAction] = re_barred | re_unbarred | re_tau
  
  def relabelVarString = agentString
  
  
  // Combines the list of prefixes into a long list of them.
  def acts: Parser[prefixB] = an_act ~ rep("." ~ an_act) ^^ {
    case curr ~ list => (curr /: list) {
      case (x, "." ~ y) => prefixB(x.prefixList ++ y.prefixList)
    }
  }
  
  def agentSymbol: Parser[PrivateAgent] = (agentString | nullAgent) ~ rep(restriction)  ^^ {
    case vName ~ rests => {
      var ag = if (vName == "0") new PNil() else new PVar(Symbol(vName))
      // Apply restrictions as they come in from the left if any.
      restrictify(ag, rests)
    }
  }
  
  // Applies restrictions from the left to the given agent. If no restrictions simply returns the original agent.
  def restrictify(givenAg: PrivateAgent, rests: List[Restriction]): PrivateAgent = {
    var ag = givenAg
    for (rest <- rests) ag = new PRestrict(CCSAgent.makeAgent(ag), rest)
    ag
  }

  //def combineGent = bracket_agent | agent_sym
  
  def restriction: Parser[Restriction] = "\\" ~ (realRestriction | bracedRestriction) ^^ {
    case _ ~ rest => rest
  }
  

  def actgent: Parser[PrivateAgent] = acts ~ "." ~ (bracketAgent | agentSymbol) ^^ {
    case prefs ~ "." ~ ag =>
      new PPrefix(prefs.prefixList, CCSAgent.makeAgent(ag))
  }
  
  // containing a single agent value e.g. a.b.0, A, 0
  def unitCCS: Parser[PrivateAgent] = bracketAgent | actgent | agentSymbol


  
  // .Agent => Agent
  def dotAgent: Parser[CCSAgent] = "." ~ unitCCS ^^ {
    case dot ~ agent => CCSAgent.makeAgent(agent)
  }
  

  
  
  def singleAgent(delim: String): Parser[CCSAgent] = delim ~ unitCCS ^^ {
    case sep ~ agent => CCSAgent.makeAgent(agent)
  }
  
  def unitParallel: Parser[CCSAgent] = singleAgent("|")
  
  def parallelAgent: Parser[PrivateAgent] = unitCCS ~ rep1(unitParallel) ^^ {
     case ag ~ listag => new PParallel(List(CCSAgent.makeAgent(ag)) ++ listag)
  }
  
  def unitSum: Parser[CCSAgent] = singleAgent("+")
  
  def sumAgent: Parser[PrivateAgent] = unitCCS ~ rep1(unitSum) ^^ {
     case ag ~ listag => new PSSum(List(CCSAgent.makeAgent(ag)) ++ listag)
  }
  
  // The string representation of a restriction is the same as an unbarred act for obvious reasons
  def restrictUnit: Parser[Value] = act ^^ {
    case a => Value.fromString(a)
  }
  
  def commaRestrict: Parser[Value] = "," ~ restrictUnit ^^ {
    case dot ~ res => res
  }
  
  
  def relabelUnit: Parser[(CCSAction, CCSAction)] = relabelAct ~ "/" ~ relabelAct ^^ {
    case to ~ _ ~ from => (to, from)
  }
  
  def commaRelabel: Parser[(CCSAction, CCSAction)] = "," ~ relabelUnit ^^ {
    case comma ~ res => res
  }
  
  // Making the parser able to go char by char by adding the end ] in relabelList and relabellingVar
  def relabelList: Parser[List[(CCSAction, CCSAction)]] = relabelUnit ~  rep(commaRelabel) ^^ {
    case one ~ lst => one :: lst
  }
  
  def unitLit: Parser[List[(CCSAction, CCSAction)]] = "[" ~ relabelList ~ "]" ^^ {
    case _ ~ lst ~ _ => lst
  }
  
  // Need to join together consecutive cases. E.g. [a/b][c/d] => [a/b, c/d]
  def partLitRelabel: Parser[LitRelabel] = relabelList~ "]" ~ rep(unitLit) ^^ {
    case unit ~ _ ~ List() => Relabeling.makeLiteralRelabelling(unit)
    case unit ~ _ ~ xss => {
      var lst = unit
      for (xs <- xss) lst = lst ++ xs
      Relabeling.makeLiteralRelabelling(lst)
    }
  }
  
  def litRelabel: Parser[LitRelabel] = "[" ~ partLitRelabel ^^ {
    case _ ~ relabel => relabel
  }
  
  
  
  
  def relabellingVar: Parser[RelabelVar] = relabelVarString ~ "]" ^^ {
    case x ~ _ => new RelabelVar(x)
  }
  
  def relabelling: Parser[Relabeling] = "[" ~ (partLitRelabel | relabellingVar) ^^ {
    case _ ~ relabelling => relabelling
  }
  
  def realRestriction: Parser[Restriction] = restrictUnit ~ rep(commaRestrict) ^^ {
    case single ~ list => new Restriction(List(single) ++ list)
  }
  
  def bracedRestriction: Parser[Restriction] = "{" ~ realRestriction ~ "}" ^^ {
    case _ ~ rest ~ _ => rest
  }
  
  
  def restrictAgent: Parser[PrivateAgent] = {
    restrictCnt += 1
    var agType = agent


  agType ~ "\\" ~ (bracedRestriction | realRestriction) ^^ {
    case ag ~ _ ~ rest => new PRestrict(CCSAgent.makeAgent(ag), rest)
  }
  }

  
  def bracketAgent: Parser[PrivateAgent] = "("  ~ agent ~ ")" ~ rep(restriction) ^^ {
    case _ ~ ag ~ _ ~ rests => {
      // Apply restrictions if any.
      restrictify(ag, rests)
    }
  }  
  
  // Relabellings always applied last to an agent definition. If none defined the "pure" agent is returned.
  def agent: Parser[PrivateAgent] = (sumAgent | parallelAgent |  unitCCS) ~ rep(relabelling) ^^ {
    case priv ~ relabelList => {
      var ag = priv
      for (r <- relabelList) ag = new PRelabel(CCSAgent.makeAgent(ag), r)
      ag
    }
  }
  
  def readAgent(input: String): CCSAgent = {
    apply(input) match {
      case a: CCSAgent => a
      case _ => throw new CWBParseException("Could not parse " + input)
    }
  }
  
  
  
  def cleanUnbarred: Parser[CCSAction] = act ^^ {
    case x => new Act(Symbol(x), true, None)
  }
  
  def cleanBarred: Parser[CCSAction] = "'" ~ act ^^ {
    case _ ~x => new Act(Symbol(x), false, None)
  }
  
  def cleanTau: Parser[CCSAction] = "tau" ^^ {
    case _ => new Tau(None)
  }
  
  def clean_act = cleanTau | cleanBarred | cleanUnbarred
  
  /**
   * Given an action string input returns the action.
   * @param input string representation of an action.
   * @return the corresponding action.
   */
  def readAct(input: String): CCSAction = {
    parseAll(clean_act, input) match {
      case Success(result, _) => result
      case failure: NoSuccess => throw new CWBParseException("Could not parse action " + input)
    }
  }
  
  
    def pairBracketAgent: Parser[(PrivateAgent, PrivateAgent)] = "(" ~ agent ~ "," ~ agent ~ ")" ^^ {
      case lb ~ ag1 ~ _ ~ ag2 ~ rb => (ag1, ag2)
    }
  
    /**
     * Given a string (agent1_def, agent2_def) returns agent1 and agent 2
     * @param input bracketed agent input
     * @return (agent1, agent2)
     */
    def getAgentPair(input: String): (CCSAgent, CCSAgent) = {
       parseAll(pairBracketAgent, input) match {
         case Success(result: (PrivateAgent, PrivateAgent), _) => (CCSAgent.makeAgent(result._1), CCSAgent.makeAgent(result._2))
         case failure: NoSuccess => throw CWBParseException(failure.msg)
       }
    }
  
  /**
   * Verifies whether the given name is a valid agent name in CCS.
   * @param name proposed agent name
   * @return name is valid CCS
   */
  def isValidAgentName(name: String) = {
    parseAll(agentString, name) match {
      case Success(_, _) => true
      case _ => false
    }
  }
  
    
  /**
    * Given an agent string definition creates and returns a newly created CCS agent
    * @param input agent definition.
    * @return the corresponding agent.
    */
  def apply(input: String): CCSAgent = {    
    parseAll(agent, input) match {
    
    case Success(result: PrivateAgent, _) => CCSAgent.makeAgent(result)
    case failure: NoSuccess => scala.sys.error(failure.msg)
    }
  }
  
  
  
}


